nLab set-theoretic multiverse

The set-theoretic multiverse

This article is about the notion of multiverse in set theory. For other notions of multiverse, see multiverse.


Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

The set-theoretic multiverse

Idea

The set-theoretic multiverse is a philosophical perspective on set theory, advocated by Joel David Hamkins, according to which

there are many distinct concepts of set, each instantiated in a corresponding set-theoretic universe.

This is in contrast to the “universe view”, which

asserts that there is an absolute background set concept, with a corresponding absolute set-theoretic universe in which every set-theoretic question has a definite answer.

The set-theoretic multiverse is at least informally analogous to such categorical notions as Topos, the 2-category of toposes, with each topos regarded as a universe of (“variable”) sets. See at topos theory and at categorical logic for more on this.

In dependent type theory

In dependent type theory, the set-theoretic multiverse is given by the existence of multiple inequivalent models of set theory as types VV with well-founded relations \in, which are made into Tarski universes via the dependent sum type:

x:VEl(x) y:Vyxx:V \vdash \mathrm{El}(x) \coloneqq \sum_{y:V} y \in x

In addition, this extends to any other notion of set theory, such as the categorical models of set theory as well-pointed categories \mathcal{E}, which are made into Tarski universes by the hom-set

x:VEl(x)hom(1,x)x:V \vdash \mathrm{El}(x) \coloneqq \mathrm{hom}(1, x)

where 1:1:\mathcal{E} is the terminal separator of the category \mathcal{E}.

This all coexists with the usual type theoretic notion of universes of sets as Tarski universes UU with universal type family TT in which for every type A:UA:U in the universe, T(A)T(A) satisfies UIP.

References

Last revised on July 2, 2025 at 16:48:31. See the history of this page for a list of all contributions to it.